Due to advances in technologies, including advances pertaining to memory, processing capabilities, storage capacity, amongst others, computers have evolved from relatively high cost, low function machines to relatively low cost machines that can perform a variety of functions, including but not limited to complex mathematical computation, detailed graphics rendering, web browsing, etc. Furthermore, portable computing devices exist that allow many of the aforementioned functions to be executed on a portable device, such as mobile telephones and/or multimedia players. Additionally, computing devices have been deployed in a variety of contexts, such as in airplanes where real-time processing of sensor data is utilized to aid in maintaining control of an airplane, in automobile navigation systems to display a current location to an operator of the automobile, etc.
Programs executing on computing devices use physical resources of such computing devices, such as memory, processing time, power of a device, bandwidth on a network, etc. In many devices and/or contexts, the physical resources of a computing device are limited and/or are desirably closely monitored. For example, in real-time systems, it is desirable to bound the worst-case execution time of a program. In a program that is to be executed on a low power device or in a low bandwidth environment, it is desirable to bound the amount of power and/or bandwidth utilized by the computing device when executing the program. Estimating such resource bounds can be undertaken by determining the number of times one or more control locations inside a program that consumes these resources are executed.
Program execution can also affect certain quantitative properties of data upon which the program operates. For instance, the amount of secret leaked by a program can depend upon the number of times that a certain operation that leaks data is executed (e.g., by either direct or indirect information flow). Additionally, an amount of perturbation in output data values resulting from a relatively small perturbation or uncertainty in input values can depend upon the number of times additive error propagation operators are applied. Estimating such quantitative properties can be undertaken by determining the number of times one or more control locations inside a program that perform certain operations are executed.
Conventional approaches for ascertaining the number of times that a control location executes in a program are relatively imprecise and conservative in nature. An example approach for computing symbolic bounds on the number of times a control location executes in a program is to estimate a bound on a closest enclosing loop using techniques for loop bound computation. Again, however, this approach tends to be conservative and imprecise.